$\forall$${\it es}$:ES, $i$:Id, ${\it e'}$:E, $P$, $R$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$). \\[0ex]es{-}first{-}at{-}since(${\it es}$;$i$;${\it e'}$;$e$.$R$($e$);$e$.$P$($e$)) $\in$ $\mathbb{P}$